T:Type, R:(TTProp). (Sym x,y:T. x R y)  (Sym x,y:T. x (R^*) y) 

latex

Definitions	Sym x,y:T. E(x;y), R^*, x:A. B(x), P  Q, x f y, Prop, t  T, R^-1, R1 => R2, P  Q, P & Q, P  Q
Lemmas	rel inverse star, rel inverse wf, rel star monotonic, rel star wf